$\forall$$T$:Type, $j$:$\mathbb{N}$, $l$:$T$ List. 0$<$$j$ $\Rightarrow$ $j$$<\parallel$$l$$\parallel$ $\Rightarrow$ ((firstn($j$$-$1;$l$) @ [$l$[$j$$-$1]]) $\sim$ firstn($j$;$l$))